#ifndef __INIT_KERNEL_H__
#define __INIT_KERNEL_H__

#include "solver_function.h"
#include "vec.h"

#ifdef RANDOM_POLARITY
__global__ void
kernel_init_rand( void )
{
	int tId = threadIdx.x;

	//printf("sizeof(curandState) = %d, &__dev_randState[%d] = %x\n", sizeof(curandState), tId, &__dev_randState[tId] );
	curand_init( __curandSeed, tId, 0, &__dev_randState[tId] );
}
#endif

// Only one block.
__global__ void
//__launch_bounds__ ( __threadsPerBlock2, 1 )
kernel_global_init_dpll_sat( void )
{
	int tId = threadIdx.x;

	if ( tId == 0 )
	{
#ifdef HALF_IDLE_BLOCK
		__dev_idleBlockCount = 0;
#endif
		__dev_hasResult = 0;
		__dev_unitClauseLitSize = __dev_unitClaNumber;
		(*__dev_clausePtrIndexSize) = __dev_claNumber;
		__dev_conflictLimit = __initialConflictLimit;
#ifndef KEEP_LEARNT_CLAUSE
		__dev_learntClauseLimit = __dev_initialLearntClauseLimit;
#endif
		__dev_claActivityIncreaseDelta = 1;
		__dev_decreaseClauseActivity = 0;
	}
	__threadfence_block();

//	for ( int i = tId; i < __blocksPerGrid; i += __threadsPerBlock2 )
//	{ curand_init( __curandSeed, i, 0, &__dev_curandState[i] ); }

	// Initializing shared unit clauses.
	for ( int i = tId; i < __dev_unitClaNumber; i += __threadsPerBlock2 )
	{
		__dev_unitVar[i] = get_unitClaArr(i).index();
		set_unitClauseLit( i, get_unitClaArr(i) );
	}

	for ( int i = tId + __dev_unitClaNumber; i < __dev_varNumber; i += __threadsPerBlock2 )
	{ __dev_unitVar[i] = -1; }

	for ( int i = tId + __dev_unitClaNumber; i < __dev_varNumber; i += __threadsPerBlock2 )
	{ __dev_unitClauseLit[i] = Lit(); }

	// Construct clauses and store their pointers in __dev_clausePtrIndex array.
	for ( int i = tId; i < __dev_claNumber; i += __threadsPerBlock2 )
	{
		int beginId = get_claArrIndex( i );
		int endId = get_claArrIndex( i + 1 );
		Clause* clausePtr = Clause_new( i, false, __dev_claArr, beginId, endId );
#ifdef ASSERT
		if ( clausePtr == NULL )
		{ printf( "kernel_global_init_dpll_sat(): assertion failed: new Clause gets NULL pointer.\n" ); }
#endif
#ifdef DEBUG_DPLL_INIT
		printf ( "New Clause: __dev_clausePtrIndex[%d] = %x\n", i, clausePtr );
#endif
		set_clausePtrIndex( i, clausePtr );
	}
	__threadfence_block();

#ifdef ASSERT
	for ( int i = tId; i < __dev_claNumber; i += __threadsPerBlock2 )
	{
		int beginId = get_claArrIndex( i );
		int endId = get_claArrIndex( i + 1 );
		Clause* clausePtr = get_clausePtrIndex(i);
#ifdef DEBUG_DPLL_INIT
		printf ( "__dev_clausePtrIndex[%d] = %x\n", i, clausePtr );
#endif
		int size = clausePtr->size();

		if ( size != (endId - beginId) )
		{ printf("kernel_global_init_dpll_sat(): Assertion failed: inconsistent clause size %d/%d between database and clause object #%d.\n", size, (endId - beginId), i ); }
		else
		{
			for ( int j = 0; j < size; ++j )
			{
				if ( (*get_claArrPointer(beginId+j)) != clausePtr->data(j) )
				{ printf("kernel_global_init_dpll_sat(): Assertion failed: inconsistent literal data between database and clause object #%d[%d] (%d/%d).\n", i, j, (*get_claArrPointer(beginId+j)).index(), (clausePtr->data(j)).index() ); }
			}
		}
	}
#endif

	return;
}

__global__ void
//__launch_bounds__ ( __threadsPerBlock, __minBlocksPerMultiprocessor )
kernel_block_init_dpll_sat( void )
{
	int tId = threadIdx.x;
	int bId = blockIdx.x;

	__shared__ Lit**			tWatchPointer;
	__shared__ Vec <Clause*>*	tWatchList;

	__shared__ Vec <Lit>* localUnitClausePtr;
	__shared__ Vec <int>* decisionLevelVarOrderPtr; // For back-tracking.
	__shared__ Vec <int>* decisionLevelTrailIdPtr; // For back-tracking.
	__shared__ Vec <Lit>* propagationQueuePtr;
	__shared__ Vec <Lit>* tempQueuePtr;
	__shared__ Vec <Clause*>* antecedentQueuePtr;
	__shared__ Vec <Clause*>* tempAntecedentPtr;
	__shared__ Vec <Clause*>* tempWatchListPtr;
	__shared__ Vec <Lit>* learntClauseLitPtr;

	if ( tId == 0 )
	{
		tWatchList = xmalloc< Vec<Clause*> > ( sizeof(Vec<int>) * __dev_litNumber );
		tWatchPointer =  (Lit**)( (char*)__dev_watchPointer + bId * __dev_watchPointerPitch );
		set_watchListPtr( bId, tWatchList );

		localUnitClausePtr = new Vec <Lit> ();
		decisionLevelVarOrderPtr = new Vec <int> ();
		decisionLevelTrailIdPtr = new Vec <int> ();
		propagationQueuePtr = new Vec <Lit> ();
		tempQueuePtr = new Vec <Lit> ();
		antecedentQueuePtr = new Vec <Clause*> ();
		tempAntecedentPtr = new Vec <Clause*> ();
		tempWatchListPtr = new Vec <Clause*> ();
		learntClauseLitPtr = new Vec <Lit> ();

		localUnitClausePtr->reserve( __dev_varNumber );
		decisionLevelVarOrderPtr->reserve( __dev_varNumber );
		decisionLevelTrailIdPtr->reserve( __dev_varNumber );
		propagationQueuePtr->reserve( __dev_varNumber );
		tempQueuePtr->reserve( __dev_varNumber );
		antecedentQueuePtr->reserve( __dev_varNumber );
		tempAntecedentPtr->reserve( __dev_varNumber );
		tempWatchListPtr->reserve( __dev_claNumber );
		learntClauseLitPtr->reserve( __dev_varNumber );

		__dev_localUnitClausePtr[bId] = localUnitClausePtr;
		__dev_decisionLevelVarOrderPtr[bId] = decisionLevelVarOrderPtr;
		__dev_decisionLevelTrailIdPtr[bId] = decisionLevelTrailIdPtr;
		__dev_propagationQueuePtr[bId] = propagationQueuePtr;
		__dev_tempQueuePtr[bId] = tempQueuePtr;
		__dev_antecedentQueuePtr[bId] = antecedentQueuePtr;
		__dev_tempAntecedentPtr[bId] = tempAntecedentPtr;
		__dev_tempWatchListPtr[bId] = tempWatchListPtr;
		__dev_learntClauseLitPtr[bId] = learntClauseLitPtr;
	}
	__threadfence_block();


	// Initialize watch pointers in this block.
	for ( int i = tId; i < __dev_claNumber; i += __threadsPerBlock )
	{
		int watchIndex = i << 1;

		tWatchPointer[watchIndex] = __dev_clausePtrIndex[i]->data_pointer(0);
		tWatchPointer[watchIndex + 1] = __dev_clausePtrIndex[i]->data_pointer(1);
#ifdef DEBUG_DPLL_INIT
		printf( "(1) tWatchPointer[%d] = %x, *tWatchPointer[%d] = %d\n", (i << 1), get_watchPointer(tWatchPointer, (i << 1) ), (i << 1), (*get_watchPointer(tWatchPointer, (i << 1) )).index() );
		printf( "(2) tWatchPointer[%d] = %x, *tWatchPointer[%d] = %d\n", ((i << 1) + 1), get_watchPointer(tWatchPointer, ((i << 1) + 1) ), ((i << 1) + 1), (*get_watchPointer(tWatchPointer, ((i << 1) + 1) )).index() );
#endif
	}
	__threadfence_block();

	// Initilize watch list.
	for ( int i = tId; i < __dev_litNumber; i += __threadsPerBlock )
	{
		new (&tWatchList[i]) Vec <Clause*>();
		tWatchList[i].reserve( __dev_claNumber >> 5 );

#ifdef DEBUG_DPLL_INIT
		printf ( "sizeof(Vec <Clause*>) = %d, tWatchList[%d] = %x\n", sizeof(Vec<Clause*>), i, &tWatchList[i] );
#endif
		for ( int j = 0; j < __dev_claNumber; ++j )
		{
			int watchIndex = j << 1;

			if ( tWatchPointer[watchIndex]->index() == i )
			{ tWatchList[i].push_back( __dev_clausePtrIndex[j] ); }

			if ( tWatchPointer[watchIndex + 1]->index() == i )
			{ tWatchList[i].push_back( __dev_clausePtrIndex[j] ); }
#ifdef ASSERT
			if ( *get_watchPointer( tWatchPointer, watchIndex ) == *get_watchPointer( tWatchPointer, (watchIndex + 1) ) )
			{ printf( "Assertion failed: tId #%d bId #%d: initilizing two watch pointers in the same clause points to the same literal.\n", tId, bId ); }
#endif
		}
	}
	__threadfence_block();

#ifdef ASSERT
	for ( int i = tId; i < __dev_litNumber; i += __threadsPerBlock )
	{
		for ( int j = 0; j < get_watchList( tWatchList, i )->size(); ++j )
		{
			if ( (tWatchPointer[tWatchList[i].at(j)->index() << 1]->index() != i)
				&& (tWatchPointer[(tWatchList[i].at(j)->index() << 1) + 1]->index() != i) )
			{
				printf( "Assertion failed: tId #%d bId #%d: Watch list of Lit #%d has other Lit #%d and #%d.\n",
					tId, bId, i,
					get_watchPointer( tWatchPointer, (get_watchList( tWatchList, i )->at(j)->index() << 1) )->index(),
					get_watchPointer( tWatchPointer, ((get_watchList( tWatchList, i )->at(j)->index() << 1) + 1) )->index()
					);
			}
		}
	}
	__threadfence_block();
#endif

#ifdef DEBUG_DPLL_INIT
	__syncthreads();
	if ( tId == 0 )
	{
		printf( "\nbId #%d, Watch list:\n", bId );
		for ( int i = 0; i < __dev_litNumber; ++i )
		{
			printf( "Lit #%d: tWatchList[%d] = %x: ", i, i, (void*)(&tWatchList[i]) );
			for ( int j = 0; j < get_watchList( tWatchList, i )->size(); ++j )
			{
				printf( "%d, ", (get_watchList( tWatchList, i )->at(j))->index() );
			}
			printf( "\n" );
		}
		printf( "\n" );
	}
	__threadfence_block();
#endif

	return;
}

#endif /* __INIT_KERNEL_H__ */